Support null-pointer without operand in interpreter #2917

mgudemann · 2018-09-07T13:31:41Z

Before the interpreter evaluate function always expected a pointer type to have an operand, but we can have NULL pointers without operand, in the example it was from cprover_string_content

allredj

Passed Diffblue compatibility checks (cbmc commit: 624d1aa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84141522

tautschnig · 2018-09-07T15:31:45Z

src/goto-programs/interpreter_evaluate.cpp

@@ -339,11 +339,19 @@ void interpretert::evaluate(
        evaluate(expr.op0(), dest);
        return;
      }
-      if(expr.has_operands() && !to_integer(expr.op0(), i))
+      else if(


Sorry, not being changed here, but as I'm trying to understand the code: line 334 suggests there is a type ID_address_of?

That surely must be in error!

I removed this (and one other occurrence) I don't think those can be types

tautschnig · 2018-09-07T15:33:02Z

src/goto-programs/interpreter_evaluate.cpp

@@ -339,11 +339,19 @@ void interpretert::evaluate(
        evaluate(expr.op0(), dest);
        return;
      }
-      if(expr.has_operands() && !to_integer(expr.op0(), i))
+      else if(
+        expr.has_operands() && !to_integer(to_constant_expr(expr.op0()), i))


What does a pointer-typed constant (mind the test in line 300) with operands even look like?

Constant memory offset? void *x = 0x100? Don't know if that is ever what you want

@tautschnig this for example

java::@inflight_exception constant * type: pointer * width: 64 * #no_nondet_initialization: 1 0: empty * value: 0000000000000000000000000000000000000000000000000000000000000000 0: constant * type: pointer * width: 64 * #no_nondet_initialization: 1 0: empty * value: NULL

effectively this here was the culprit for the failed to evaluate expression: null:

cprover_string_content::cprover_string_content constant * type: pointer * width: 64 0: unsignedbv * width: 16 * value: NULL * #source_location: * file: org/apache/tika/parser/prt/PRTParser.java * line: 222 * function: java::org.apache.tika.parser.prt.PRTParser.extractText:([BZ)Ljava/lang/String; * java_bytecode_index: 22 !! failed to evaluate expression: null

(both first name then .pretty output)

That is definitely wrong (!) Could you raise a ticket either on issues here or on Jira to track this down. @LAJW I bet this is why you had some weird edge case handling code for null pointers!

tautschnig · 2018-09-07T15:35:27Z

src/goto-programs/interpreter_evaluate.cpp

+      // check if expression is constant null pointer without operands
+      else if(
+        !expr.has_operands() && !to_integer(to_constant_expr(expr), i) &&
+        i == 0)


You might just do expr.is_zero(), although config.ansi_c.NULL_is_zero should actually be considered.

made it i.is_zero() I am not sure that java correctly sets the NULL_is_zero in any case

allredj

Passed Diffblue compatibility checks (cbmc commit: 8b3bfaa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84148025

allredj

Passed Diffblue compatibility checks (cbmc commit: 56ef1d4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84153742

thk123

I don't know how feasible this is, but I have no idea what this change does so it'd be great to ad a (unit?) test.

mgudemann · 2018-09-10T14:26:58Z

@thk123 this fixes an error message from the interpreter. It should be possible to call the evaluate method f the interpreter and to check the result.

allredj

Passed Diffblue compatibility checks (cbmc commit: 55a1dfe).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84304603

smowton · 2018-09-11T08:45:44Z

I don't have a strong opinion which one we want, but surely there should be one correct form of a null pointer constant, and the interpreter should understand that one form?

@tautschnig the "operand" form is I believe inspired by the constant object pointers produced by prop_convt::get, which will make something like 0x100 (operand &obj_xyz), thus providing both the address and the meaning of that address. The null with operands is giving the numerical representation (0) and the symbolic one (null).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: bce73d4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84403064
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

thk123 · 2018-09-11T10:17:35Z

@smowton - thanks for this that makes sense. But null_pointer_exprt returns the no-operand version - so it should be updated to return this op'd version if this is really is the "correct" format for a pointer. This should also be documented (perhaps in pointer_typet/null_pointer_exprt/address_of_exprt)

thk123

Thanks for the test!

💡 can we get one for the other kind of null pointer too?
🚫 avoid putting code only required for test in the main src

thk123 · 2018-09-11T10:18:08Z

src/goto-programs/interpreter_class.h

@@ -306,6 +306,14 @@ class interpretert:public messaget

  void initialize(bool init);
  void show_state();
+
+  friend mp_vectort


🚫 This is required for the unit test right? I think it is cleaner to declare friend class interpreter_testt and then put this into the unit folder 0 as it stands you might as well make evaluate public no?

will go with the friend class, that is hopefully less controversial

thk123 · 2018-09-11T10:23:07Z

unit/interpreter/interpreter.cpp

+  interpretert::mp_vectort mp_vector =
+    interpreter_evaluate(interpreter, constant_expr);
+
+  REQUIRE(mp_vector.size() == 1);


⛏️ You can use

REQUIRE_THAT(mp_vector, Catch::Matchers::Vector::Equals<mp_integer>{{0}});

To check that the array is exactly {0}

smowton · 2018-09-11T10:59:16Z

It might be better to say there is a correct format in a particular place. The interpreter operates over traces, which have been produced by prop_convt::get'ing all the symbols in a particular equation. My guess is it's behaving differently for constants given in the input equation vs. symbols that have been solved for a zero / null value.

mgudemann · 2018-09-11T12:31:05Z

@thk123 addressed your comments

allredj

This PR failed Diffblue compatibility checks (cbmc commit: d4f9fb0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84421606
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

majakusber · 2018-09-11T15:58:05Z

src/goto-programs/interpreter_evaluate.cpp

@@ -339,7 +339,16 @@ void interpretert::evaluate(
        evaluate(expr.op0(), dest);
        return;
      }
-      if(expr.has_operands() && !to_integer(expr.op0(), i))
+      else if(


Since all of the if/else if return, you can make them all ifs.

src/goto-programs/interpreter_evaluate.cpp

allredj

Passed Diffblue compatibility checks (cbmc commit: d22f26a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84449831

Result was moved twice instead of initializing `input` field with the given `input`.

allredj

Passed Diffblue compatibility checks (cbmc commit: 7bc468d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84545908

mgudemann · 2018-09-12T12:15:26Z

based on #2935

allredj

Passed Diffblue compatibility checks (cbmc commit: f7e9715).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84558263

mgudemann requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners September 7, 2018 13:31

mgudemann self-assigned this Sep 7, 2018

allredj reviewed Sep 7, 2018

View reviewed changes

mgudemann force-pushed the fix/interpreter/null_pointer_no_operand branch from 624d1aa to 8b3bfaa Compare September 7, 2018 15:29

tautschnig reviewed Sep 7, 2018

View reviewed changes

allredj reviewed Sep 7, 2018

View reviewed changes

mgudemann force-pushed the fix/interpreter/null_pointer_no_operand branch from 8b3bfaa to 56ef1d4 Compare September 7, 2018 16:40

allredj reviewed Sep 7, 2018

View reviewed changes

thk123 reviewed Sep 10, 2018

View reviewed changes

mgudemann force-pushed the fix/interpreter/null_pointer_no_operand branch from 56ef1d4 to 55a1dfe Compare September 10, 2018 14:17

allredj reviewed Sep 10, 2018

View reviewed changes

mgudemann force-pushed the fix/interpreter/null_pointer_no_operand branch from 4524b08 to d7b43f2 Compare September 11, 2018 08:25

mgudemann force-pushed the fix/interpreter/null_pointer_no_operand branch 2 times, most recently from b684a94 to bce73d4 Compare September 11, 2018 09:26

allredj reviewed Sep 11, 2018

View reviewed changes

thk123 reviewed Sep 11, 2018

View reviewed changes

mgudemann force-pushed the fix/interpreter/null_pointer_no_operand branch from bce73d4 to d4f9fb0 Compare September 11, 2018 12:24

allredj reviewed Sep 11, 2018

View reviewed changes

thk123 approved these changes Sep 11, 2018

View reviewed changes

mgudemann force-pushed the fix/interpreter/null_pointer_no_operand branch from d4f9fb0 to d22f26a Compare September 11, 2018 14:47

majakusber reviewed Sep 11, 2018

View reviewed changes

allredj reviewed Sep 11, 2018

View reviewed changes

peterschrammel approved these changes Sep 11, 2018

View reviewed changes

Correct input initialization in builtin function

7857669

Result was moved twice instead of initializing `input` field with the given `input`.

mgudemann force-pushed the fix/interpreter/null_pointer_no_operand branch from d22f26a to 7bc468d Compare September 12, 2018 09:41

majakusber approved these changes Sep 12, 2018

View reviewed changes

allredj reviewed Sep 12, 2018

View reviewed changes

Matthias Güdemann added 3 commits September 12, 2018 14:03

Support null-pointer without operand in interpreter

207ca8c

Remove ID_address_of check for types as it can only be exprt

df6c64f

Add unit test for interpreter evaluation

f7e9715

mgudemann force-pushed the fix/interpreter/null_pointer_no_operand branch from 7bc468d to f7e9715 Compare September 12, 2018 12:04

mgudemann requested review from martin-cs and romainbrenguier as code owners September 12, 2018 12:04

allredj reviewed Sep 12, 2018

View reviewed changes

peterschrammel mentioned this pull request Sep 12, 2018

Correct input initialization in builtin function #2935

Merged

mgudemann merged commit 8863b9c into diffblue:develop Sep 13, 2018

mgudemann deleted the fix/interpreter/null_pointer_no_operand branch September 13, 2018 07:48

Support null-pointer without operand in interpreter #2917

Support null-pointer without operand in interpreter #2917

Uh oh!

Conversation

mgudemann commented Sep 7, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mgudemann Sep 10, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

mgudemann commented Sep 10, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Sep 11, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 commented Sep 11, 2018

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Sep 11, 2018

Uh oh!

mgudemann commented Sep 11, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

mgudemann commented Sep 12, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

mgudemann Sep 10, 2018 •

edited

Loading